\begin{tabbing}
qrng
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$rationals\+
\\[0ex], $\lambda$$x$,$y$. qeq($x$; $y$)
\\[0ex], $\lambda$$x$,$y$. q\_le($x$; $y$)
\\[0ex], $\lambda$$x$,$y$. $x$ + $y$
\\[0ex], 0
\\[0ex], $\lambda$$x$.({-}1) $\ast$ $x$
\\[0ex], $\lambda$$x$,$y$. $x$ $\ast$ $y$
\\[0ex], 1
\\[0ex], $\lambda$$x$,$y$. if qeq($y$; 0) then inr $\cdot$  else inl qdiv($x$; $y$)  fi $>$
\-
\end{tabbing}